In this paper we consider the problem of computing the optimal (minimum ormaximum) expected time to reach a target and the synthesis of an optimalcontroller for a probabilistic timed automaton (PTA). Although this problemadmits solutions that employ the digital clocks abstraction or statistical modelchecking, symbolic methods based on zones and priced zones fail due to thedifficulty of incorporating probabilistic branching in the context of dense time.We work in a generalisation of the setting introduced by Asarin and Maler forthe corresponding problem for timed automata, where simple and nice functionsare introduced to ensure finiteness of the dense-time representation. We findrestrictions sufficient for value iteration to converge to the optimal expectedtime on the uncountable Markov decision process representing the semantics ofa PTA. We formulate Bellman operators on the backwards zone graph of a PTAand prove that value iteration using these operators equals that computed overthe PTA’s semantics. This enables us to extract an ε-optimal controller fromvalue iteration in the standard way.
展开▼
